agree_on(T;x.P(x))(L1,L2)
== ||L1|| = ||L2|| & (i:||L1||. P(L1[i])  P(L2[i])  L1[i] = L2[i]) 

latex

---

clarification:

agree_on(T;x.P(x))(L1,L2)
== ||L1|| = ||L2||   & (i:{0..||L1||}. P(L1[i])  P(L2[i])  L1[i] = L2[i]  T) 

latex

Definitions	A & B, x:A. B(x), {i..j}, ||as||, P  Q, P  Q, l[i]
FDL editor aliases	agree_on